Reductions from RAM to Circuit Satisfiability
https://gyazo.com/91d008afc02dcbeabd969aaf1076ef3c
TinyRAMからCircuitへの変換
https://github.com/scipr-lab/libsnark/blob/master/libsnark/gadgetlib1/gadgets/cpu_checkers/tinyram/tinyram_cpu_checker.tcc
https://github.com/scipr-lab/libsnark/tree/master/libsnark/reductions/ram_to_r1cs
1. tinyRAM
http://web.eecs.umich.edu/~genkin/papers/ramreduce-20120818.pdf
ハーバードアーキテクチャ型RISC
命令とmemoryを別々に格納
code consistencyとmemory consistencyのマッチング検証のためにベネシュネットワークを利用。
https://github.com/scipr-lab/libsnark/blob/master/libsnark/gadgetlib1/gadgets/routing/benes_routing_gadget.tcc
.$ O(T(\log{T})^2)
tinyRAMの構造
レジスタとmemoryはそれぞれW bits
K個のレジスタと２個の特殊レジスタ（プログラムカウンタ・flag）
アドレスでアクセス可能なmemory
inputのreadは1回のみ
primary input tape : public input
auxiliary input tape : witness
https://gyazo.com/ae0e056a60d4d911bc4d301306eff534
tinyRAMのinstruction set
https://gyazo.com/9e65d5f30d4c04c8fb9d37c2f1101a23
x86/ARM/AVRとtinyRAMの同じプログラムに対するinstruction数の比較
コードサイズはだいたい3倍以下
https://gyazo.com/33ddcf3813bbc7fda6cff5c4606763a3
x86との実行時間の比較
実行時間はだいたい4倍以下
https://gyazo.com/22507305dc78135eb5803ef7c98cc411
tinyRAMにおけるcode consistensyとMemory consistensy。
https://youtu.be/nS3smRAfUd8
タイムステップごとに状態遷移をチェック
https://gyazo.com/036f12dc90ab4a21ddb8c363834a9b47
状態遷移とは別に、「memoryのあるアドレスにstoreした値がloadした値と一致しているか」などのチェックが必要。
しかし、全てのステップにおいて全てのmemory dataのスナップショットを保持する戦略だと、circuit複雑性が非効率。
https://gyazo.com/9b01bac12bb7ad6b7f72b21083143193
アドレスごとにinstructionをソートし、loadする値が一致しているか検証
https://gyazo.com/af14cd9f5ec13e24ffbc444cc6ace9aa
タイムステップごとにcode consistencyとmemory consistencyがソーティングされる制限も加える。
circuitをシンプルにするためにベネシュネットワークを利用。
https://gyazo.com/e2575b7acfc35ac476df16b4e830648b
プログラムのコードを行数ごとに追っていくCode ConsistencyのためのCircuit
MemoryのAddress順に追っていくMemory ConsistencyのためのCircuit
それらのCircuit同士のConsistencyを得るためのCircuit
の3つのsub-circuitに分ける。
さらに、+ boundary constraints = witness mapの生成
（$ |C| =O((T+l)\log(T+l)) in vnTinyRAM）
ALUチェックのACIPs。
以下のようにopcodeに対応する多項式がイコールゼロになれば、instructionが正しいことの制約充足問題。
circuit complexityのパラメタ
variableの数
多項式の次数
多項式の数
https://gyazo.com/53e40afbb27966b9fb2de7a790856cd2https://gyazo.com/4a6b4a899dd048e5588966b74c22e9da
2. vnTinyRAM
https://eprint.iacr.org/2013/879.pdf
https://eprint.iacr.org/2014/595.pdf で上記設計にcycles of elliptic curvesを加えることで拡張
https://blog.plan99.net/vntinyram-7b9d5b299097 : Mike Hearn blog
ノイマン型RISC
命令とdataをひとつのmemoryに格納
同じrouting networkを利用することで、instruction fetchの正当性とmemory accessの正当性を同時に検証。
waksmanネットワークを利用
https://github.com/scipr-lab/libsnark/blob/master/libsnark/gadgetlib1/gadgets/routing/as_waksman_routing_gadget.tcc
.$ O((T+l)\log(T+l))
3. using in vRAM
https://eprint.iacr.org/2018/380.pdf で提案。
http://web.eecs.umich.edu/~genkin/papers/vram.pdf
.$ O(\log(T+l))
interactive
proof size: 200kb
左がvnTinyRAM仕様、右がvRAM新提案仕様
https://gyazo.com/b72b3abd1d537ecc5f79757ed89e44b3
trace $ tr = (S_1, I_1, S_2, I_2,...,I_{T-1},S_T)
2-D : vnTinyRAM
Correct Instruction Execution
Code Consistencyの部分。
ステップ順の検証。
$ I_iのInstruction実行により状態$ S_iから$ S_{i+1}が得られるか。
なので、$ C_{exe}に$ S_i, I_i, I_{i+1}がinputとして与えられる。
以下を検証
状態$ S_iでの値$ O_iがinstruction $ I_iによって正しく計算されているか
.$ I_iがmemory loadの場合は、loadされた値$ O_iが正しいと仮定。
memory accessのテストで検証される
値$ O_iが状態$ S_{i+1}の$ r_jに一致しているか
jump opの時は、$ pc_{i+1}に一致しているか
.$ S_{i+1}の他の全てのレジスタは$ S_iと同じか
.$ S_iのStep number (T) は$ iと同じか
.$ pc_iはプログラムPのinstruction$ I_iの行数と同じか
Correct Instruction Fetches
instruction$ I_iが状態$ S_iでプログラムPにおけるprogram counterで指定されたinstructionであるかどうか。
もし$ i=1ならpc=0。
MemoryにプログラムPをstoreし、それらを実行する前にinstructionをloadする。
上述のtraceの前にプログラムをstoreする$ B_iを加える。
つまり、$ B_iはプログラムPのi番目のinstructionをアドレスiのメモリにstore。
$ tr = (B_1, ..., B_l,S_1, I_1, S_2, I_2,...,I_{T-1},S_T)
となり、長さは$ 2T+l
これにより、ひとつのInstruction$ I_iは2つのoperationと見なすことができる。
行数指定のmemory addressからinstructionを見て、operationをloadする
instruction$ I_iの操作それ自体
よって、instructionのfetchの正当性は下記のmemory storeとloadのconsistencyをチェックすればOK。
Correct Memory Accesses
$ I_iがmemoryのaddress $ aにアクセスするload instructionで、そのloadされる値$ vが以前のinstructionによってaddress $ aに書き込まれた最新の値であるかどうか。
以下のルールで並び替えた追加traceをwitnessに含める。
$ tr^* = (A_1,...A_{2T+l})
アクセスするmemory アドレス$ a順に並び替え
memoryに関係のないinstructionはtraceの一番最後に並び替え
このtrace*を用いて$ C_{mem}は以下を検証
code stepベースで続けてアクセスするアドレスが同じ（$ a_i = a _{i+1})である場合。
もし、新しい方がload instructionであるなら、loadされた値はひとつ前のinstructionでstoreあるいはloadされる値と同じであるか
memory addressが違う場合
.$ A_{i+1}のload instructionで得られる値は0であるか
traceとtrace*のconsistencyチェック
上記で正しくtr*がソートされているかの検証はされているので、全てのtr*がtrとマッチングするか検証するだけ。
permutation$ \piで指定されたネットワークをswitchingするcontrol bitsはProverにより提供されwitnessに含まれる。
任意サイズのwaksman networkを利用
https://hal.inria.fr/inria-00072871/document
using in vRAM
Proverの複雑性を上記の$ O((T+l)\log(T+l))から$ O(\log(T+l))に削減。
https://eprint.iacr.org/2018/380.pdf で提案。
上記提案ベースにvRAMで利用。
interactiveかつcircuitに依存しないpreproccessingフェーズを加えることで、Proverはそれぞれのstepで特定のinputのRAMプログラムによって処理されるinstructionの実行が正しいかのみを証明するだけでOKになる。
Fiat-Shamir heuristicを使ったRAMにおいてはnon-interactiveにすることが可能？
Correct Instruction Execution
Correct Instruction Fetches
Correct Memory Accesses